Inference at * 1 
Iof proof for Lemma adjacent-before:



1. T : Type
2. L : T List
3. x : T
4. y : T
5. i : {0..(||L|| - 1)}
6. x = L[i]
7. y = L[(i+1)]
  f:{0..2}{0..||L||}. (increasing(f;2) & (j:{0..2}. [x; y][j] = L[(f(j))])) 

latex

 by ((((InstConcl [j.if (j = 0) then i else i+1 fi ]) 
CollapseTHENA (Auto'))) 
CollapseTHEN (
C((RepUR ``increasing`` ( 0)) 
CollapseTHEN (MaAuto)))) 

latex

C1: 

C1: 8. i@0 : {0..1}
C1:   if (i@0 = 0) then i else i+1 fi  < if (i@0+1 = 0) then i else i+1 fi 
C2: 

C2: 8. i@0:{0..1}. if (i@0 = 0) then i else i+1 fi  < if (i@0+1 = 0) then i else i+1 fi 
C2: 9. j : {0..2}
C2:   [x; y][j] = L[if (j = 0) then i else i+1 fi ]
C.

Definitions	x.A(x), if b then t else f fi , (i = j), n+m, #$n, x:A. B(x), increasing(f;k), A c B, i  j , [car / cdr], [], A, False, P  Q, -n, , n - m, ||as||, <a, b>, l[i], {i..j}, type List, , {x:A| B(x)} , i  j < k, P & Q, x:A  B(x), x:A. B(x), x:AB(x), , Type, A  B, s = t, t  T, a < b
Lemmas	increasing wf, ifthenelse wf, int seg wf, le wf